T:Type, L:T List, x1, x2, y1, y2:T. same_order(x1;y1;x2;y2;L;T)  Prop 

latex

Definitions	t  T, x:A. B(x), x << y  l, (x  l), Prop, P  Q, same_order(x1;y1;x2;y2;L;T)
Lemmas	l member wf, strong before wf